$\forall$${\it MA}$:MsgA, $s$:${\it MA}$.state, $k$:Knd, $l$:IdLnk, ${\it vaal}$:${\it MA}$.V($k$).
\\[0ex]$\neg$${\it MA}$ sends on link $l$ $\Rightarrow$ (filter($\lambda$${\it ms}$.eqof(IdLnkDeq)(mlnk(${\it ms}$),$l$);${\it MA}$.sends($k$,$s$,${\it vaal}$)) $\sim$ nil)